Nuprl Lemma : ma-outlinks-wf2
0,22
postcript
pdf
M
:MsgAForm,
i
:Id. ma-outlinks(
M
;
i
)
(IdLnk
Id
Type) List
latex
Definitions
MsgAForm
,
ma-outlinks(
M
;
i
)
,
da-outlinks(
da
;
i
)
,
x
:
A
.
B
(
x
)
,
t
T
,
Id
Lemmas
Id
wf
,
da-outlinks
wf
,
msg-form
wf
origin
M:MsgAForm, i:Id. ma-outlinks(M;i) 
(IdLnk
IdType) List M:MsgAForm, i:Id. ma-outlinks(M;i) (IdLnkIdType) List x:A. B(x) T